TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> l , append(l1, l2) -> ifappend(l1, l2, is_empty(l1)) , ifappend(l1, l2, true()) -> l2 , ifappend(l1, l2, false()) -> cons(hd(l1), append(tl(l1), l2)) } Obligation: innermost runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 10.0 seconds. Arrrr..